YES 22.252 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule List
  ((elemIndex :: Ratio Int  ->  [Ratio Int ->  Maybe Int) :: Ratio Int  ->  [Ratio Int ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (\vv1 ->
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []
) (zip xs (enumFrom 0))


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : _) Just a



Lambda Reductions:
The following Lambda expression
\vv1
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices0 p vv1 = 
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

The following Lambda expression
\ab→(a,b)

is transformed to
zip0 a b = (a,b)



↳ HASKELL
  ↳ LR
HASKELL
      ↳ CR

mainModule List
  ((elemIndex :: Ratio Int  ->  [Ratio Int ->  Maybe Int) :: Ratio Int  ->  [Ratio Int ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : _) Just a



Case Reductions:
The following Case expression
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices00 p (x,i) = if p x then i : [] else []
findIndices00 p _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
HASKELL
          ↳ IFR

mainModule List
  ((elemIndex :: Ratio Int  ->  [Ratio Int ->  Maybe Int) :: Ratio Int  ->  [Ratio Int ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,i if p x then i : [] else []
findIndices00 p _ []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : _) Just a



If Reductions:
The following If expression
if p x then i : [] else []

is transformed to
findIndices000 i True = i : []
findIndices000 i False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
HASKELL
              ↳ BR

mainModule List
  ((elemIndex :: Ratio Int  ->  [Ratio Int ->  Maybe Int) :: Ratio Int  ->  [Ratio Int ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p _ []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : _) Just a



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
HASKELL
                  ↳ COR

mainModule List
  ((elemIndex :: Ratio Int  ->  [Ratio Int ->  Maybe Int) :: Ratio Int  ->  [Ratio Int ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : vxJust a



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
HASKELL
                      ↳ NumRed

mainModule List
  ((elemIndex :: Ratio Int  ->  [Ratio Int ->  Maybe Int) :: Ratio Int  ->  [Ratio Int ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : vxJust a



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
HASKELL
                          ↳ Narrow

mainModule List
  (elemIndex :: Ratio Int  ->  [Ratio Int ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude

  elemIndex :: Eq a => a  ->  [a ->  Maybe Int
elemIndex x findIndex (== x)

  findIndex :: (a  ->  Bool ->  [a ->  Maybe Int
findIndex p Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool ->  [a ->  [Int]
findIndices p xs concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero)))

  
findIndices0 p vv1 findIndices00 p vv1

  
findIndices00 p (x,ifindIndices000 i (p x)
findIndices00 p vw []

  
findIndices000 i True i : []
findIndices000 i False []


module Maybe where
  import qualified List
import qualified Prelude

  listToMaybe :: [a ->  Maybe a
listToMaybe [] Nothing
listToMaybe (a : vxJust a



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe1(wz217, Succ(wz2180), Zero, wz220, :(wz2210, wz2211), wz222) → new_listToMaybe(wz220, wz2210, wz2211, new_primPlusNat(wz222), new_primPlusNat(wz222))
new_listToMaybe2(wz243, wz220, wz22101, wz2211) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
new_listToMaybe(wz220, :%(Pos(Zero), Pos(wz221010)), wz2211, wz244, wz243) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
new_listToMaybe1(wz217, Succ(wz2180), Succ(wz2190), wz220, wz221, wz222) → new_listToMaybe1(wz217, wz2180, wz2190, wz220, wz221, wz222)
new_listToMaybe0(wz217, wz220, :(wz2210, wz2211), wz222) → new_listToMaybe(wz220, wz2210, wz2211, new_primPlusNat(wz222), new_primPlusNat(wz222))
new_listToMaybe(wz220, :%(Neg(Succ(wz2210000)), wz22101), wz2211, wz244, wz243) → new_listToMaybe2(wz243, wz220, wz22101, wz2211)
new_listToMaybe(wz220, :%(Neg(Zero), wz22101), wz2211, wz244, wz243) → new_listToMaybe3(wz243, wz220, wz22101, wz2211)
new_listToMaybe3(wz243, wz220, Neg(Zero), wz2211) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
new_listToMaybe(wz220, :%(Pos(Zero), Neg(Succ(wz2210100))), wz2211, wz244, wz243) → new_listToMaybe1(wz243, wz220, wz2210100, wz220, wz2211, wz243)
new_listToMaybe(wz220, :%(Pos(Succ(wz2210000)), wz22101), wz2211, wz244, wz243) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
new_listToMaybe1(wz217, Zero, Succ(wz2190), wz220, wz221, wz222) → new_listToMaybe0(wz217, wz220, wz221, wz222)
new_listToMaybe3(wz243, wz220, Neg(Succ(wz2210100)), wz2211) → new_listToMaybe1(wz243, wz220, wz2210100, wz220, wz2211, wz243)
new_listToMaybe(wz220, :%(Pos(Zero), Neg(Zero)), wz2211, wz244, wz243) → new_listToMaybe0(wz243, wz220, wz2211, wz243)
new_listToMaybe3(wz243, wz220, Pos(wz221010), wz2211) → new_listToMaybe0(wz243, wz220, wz2211, wz243)

The TRS R consists of the following rules:

new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe6(wz210, Succ(wz2110), Zero, wz213, :(wz2140, wz2141), wz215) → new_listToMaybe4(wz213, wz2140, wz2141, new_primPlusNat(wz215), new_primPlusNat(wz215))
new_listToMaybe4(wz213, :%(Neg(Succ(wz2140000)), wz21401), wz2141, wz242, wz241) → new_listToMaybe7(wz241, wz213, wz21401, wz2141)
new_listToMaybe5(wz210, wz213, :(wz2140, wz2141), wz215) → new_listToMaybe4(wz213, wz2140, wz2141, new_primPlusNat(wz215), new_primPlusNat(wz215))
new_listToMaybe8(wz241, wz213, Pos(Succ(wz2140100)), wz2141) → new_listToMaybe6(wz241, wz213, wz2140100, wz213, wz2141, wz241)
new_listToMaybe4(wz213, :%(Pos(Zero), Pos(Succ(wz2140100))), wz2141, wz242, wz241) → new_listToMaybe6(wz241, wz213, wz2140100, wz213, wz2141, wz241)
new_listToMaybe4(wz213, :%(Neg(Zero), wz21401), wz2141, wz242, wz241) → new_listToMaybe8(wz241, wz213, wz21401, wz2141)
new_listToMaybe8(wz241, wz213, Pos(Zero), wz2141) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe8(wz241, wz213, Neg(wz214010), wz2141) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe4(wz213, :%(Pos(Zero), Pos(Zero)), wz2141, wz242, wz241) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe6(wz210, Succ(wz2110), Succ(wz2120), wz213, wz214, wz215) → new_listToMaybe6(wz210, wz2110, wz2120, wz213, wz214, wz215)
new_listToMaybe4(wz213, :%(Pos(Zero), Neg(wz214010)), wz2141, wz242, wz241) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe7(wz241, wz213, wz21401, wz2141) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe4(wz213, :%(Pos(Succ(wz2140000)), wz21401), wz2141, wz242, wz241) → new_listToMaybe5(wz241, wz213, wz2141, wz241)
new_listToMaybe6(wz210, Zero, Succ(wz2120), wz213, wz214, wz215) → new_listToMaybe5(wz210, wz213, wz214, wz215)

The TRS R consists of the following rules:

new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe12(wz62, Neg(Succ(wz3100)), Pos(wz411010), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
new_listToMaybe12(wz62, Neg(Zero), Neg(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
new_listToMaybe9(Neg(Zero), :%(Pos(Zero), Pos(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
new_listToMaybe9(Pos(Zero), :%(Pos(Zero), Neg(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
new_listToMaybe9(Neg(Succ(wz3100)), :%(Pos(Zero), Pos(wz411010)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
new_listToMaybe9(wz31, :%(Pos(Succ(wz4110000)), wz41101), :(wz41110, wz41111), wz62, wz63) → new_listToMaybe9(wz31, wz41110, wz41111, new_primPlusNat(wz63), new_primPlusNat(wz63))
new_listToMaybe9(Pos(Succ(wz3100)), :%(Pos(Zero), Neg(wz411010)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
new_listToMaybe9(wz31, :%(Neg(Zero), wz41101), wz4111, wz62, wz63) → new_listToMaybe12(wz62, wz31, wz41101, wz4111, wz63)
new_listToMaybe9(Neg(Succ(wz3100)), :%(Pos(Zero), Neg(Zero)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
new_listToMaybe10(wz62, wz31, :(wz41110, wz41111), wz63) → new_listToMaybe9(wz31, wz41110, wz41111, new_primPlusNat(wz63), new_primPlusNat(wz63))
new_listToMaybe12(wz62, Pos(Zero), Pos(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
new_listToMaybe12(wz62, Pos(Succ(wz3100)), Neg(wz411010), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
new_listToMaybe9(Pos(Zero), :%(Pos(Zero), Pos(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
new_listToMaybe11(wz62, wz31, wz41101, :(wz41110, wz41111), wz63) → new_listToMaybe9(wz31, wz41110, wz41111, new_primPlusNat(wz63), new_primPlusNat(wz63))
new_listToMaybe9(Neg(Zero), :%(Pos(Zero), Neg(Succ(wz4110100))), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
new_listToMaybe12(wz62, Neg(Succ(wz3100)), Neg(Zero), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Succ(wz3100)), wz4111, wz63)
new_listToMaybe12(wz62, Pos(Zero), Neg(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Zero), wz4111, wz63)
new_listToMaybe9(Pos(Succ(wz3100)), :%(Pos(Zero), Pos(Zero)), wz4111, wz62, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
new_listToMaybe12(wz62, Neg(Zero), Pos(Succ(wz4110100)), wz4111, wz63) → new_listToMaybe10(wz62, Neg(Zero), wz4111, wz63)
new_listToMaybe12(wz62, Pos(Succ(wz3100)), Pos(Zero), wz4111, wz63) → new_listToMaybe10(wz62, Pos(Succ(wz3100)), wz4111, wz63)
new_listToMaybe9(wz31, :%(Neg(Succ(wz4110000)), wz41101), wz4111, wz62, wz63) → new_listToMaybe11(wz62, wz31, wz41101, wz4111, wz63)

The TRS R consists of the following rules:

new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe15(wz272, Zero, Zero, Pos(Zero), Neg(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Zero), wz278, wz272)
new_listToMaybe14(wz167, wz168, wz169, wz170, :(wz1710, wz1711), wz172) → new_listToMaybe13(wz170, wz168, wz1710, wz1711, new_primPlusNat(wz172), new_primPlusNat(wz172))
new_listToMaybe15(wz272, Zero, Zero, Pos(Succ(wz27500)), Pos(Succ(wz27600)), wz277, wz278) → new_listToMaybe17(wz272, wz27500, wz27600, wz277, wz27500, wz278)
new_listToMaybe18(wz311, Succ(wz3120), Succ(wz3130), wz314, wz315, wz316) → new_listToMaybe18(wz311, wz3120, wz3130, wz314, wz315, wz316)
new_listToMaybe15(wz272, Zero, Zero, Pos(Zero), Pos(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Zero), wz278, wz272)
new_listToMaybe13(wz170, wz168, :%(Neg(Zero), wz17101), wz1711, wz188, wz187) → new_listToMaybe14(wz187, wz168, wz17101, wz170, wz1711, wz187)
new_listToMaybe15(wz272, Zero, Zero, Pos(Succ(wz27500)), Pos(Zero), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Succ(wz27500)), wz278, wz272)
new_listToMaybe18(wz311, Zero, Succ(wz3130), wz314, wz315, wz316) → new_listToMaybe16(wz311, wz314, Neg(Succ(wz315)), wz316, wz311)
new_listToMaybe18(wz311, Succ(wz3120), Zero, wz314, wz315, wz316) → new_listToMaybe16(wz311, wz314, Neg(Succ(wz315)), wz316, wz311)
new_listToMaybe13(wz170, wz168, :%(Pos(wz171000), wz17101), wz1711, wz188, wz187) → new_listToMaybe14(wz187, wz168, wz17101, wz170, wz1711, wz187)
new_listToMaybe15(wz272, Succ(wz2730), Zero, wz275, wz276, wz277, wz278) → new_listToMaybe14(wz272, wz275, wz276, wz277, wz278, wz272)
new_listToMaybe15(wz272, Zero, Succ(wz2740), wz275, wz276, wz277, wz278) → new_listToMaybe14(wz272, wz275, wz276, wz277, wz278, wz272)
new_listToMaybe15(wz272, Zero, Zero, Neg(Zero), Neg(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Zero), wz278, wz272)
new_listToMaybe13(wz170, wz168, :%(Neg(Succ(wz1710000)), wz17101), wz1711, wz188, wz187) → new_listToMaybe15(wz187, wz170, wz1710000, wz168, wz17101, wz170, wz1711)
new_listToMaybe15(wz272, Zero, Zero, Neg(Zero), Pos(Succ(wz27600)), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Zero), wz278, wz272)
new_listToMaybe17(wz304, Succ(wz3050), Zero, wz307, wz308, wz309) → new_listToMaybe16(wz304, wz307, Pos(Succ(wz308)), wz309, wz304)
new_listToMaybe17(wz304, Zero, Succ(wz3060), wz307, wz308, wz309) → new_listToMaybe16(wz304, wz307, Pos(Succ(wz308)), wz309, wz304)
new_listToMaybe15(wz272, Zero, Zero, Pos(Succ(wz27500)), Neg(wz2760), wz277, wz278) → new_listToMaybe16(wz272, wz277, Pos(Succ(wz27500)), wz278, wz272)
new_listToMaybe15(wz272, Zero, Zero, Neg(Succ(wz27500)), Neg(Zero), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Succ(wz27500)), wz278, wz272)
new_listToMaybe15(wz272, Zero, Zero, Neg(Succ(wz27500)), Pos(wz2760), wz277, wz278) → new_listToMaybe16(wz272, wz277, Neg(Succ(wz27500)), wz278, wz272)
new_listToMaybe15(wz272, Zero, Zero, Neg(Succ(wz27500)), Neg(Succ(wz27600)), wz277, wz278) → new_listToMaybe18(wz272, wz27500, wz27600, wz277, wz27500, wz278)
new_listToMaybe16(wz167, wz170, wz168, :(wz1710, wz1711), wz172) → new_listToMaybe13(wz170, wz168, wz1710, wz1711, new_primPlusNat(wz172), new_primPlusNat(wz172))
new_listToMaybe15(wz272, Succ(wz2730), Succ(wz2740), wz275, wz276, wz277, wz278) → new_listToMaybe15(wz272, wz2730, wz2740, wz275, wz276, wz277, wz278)
new_listToMaybe17(wz304, Succ(wz3050), Succ(wz3060), wz307, wz308, wz309) → new_listToMaybe17(wz304, wz3050, wz3060, wz307, wz308, wz309)

The TRS R consists of the following rules:

new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe19(wz31, :%(Neg(Zero), wz411101), wz41111, wz135, wz134) → new_listToMaybe24(wz134, wz31, wz411101, wz41111)
new_listToMaybe19(Neg(Succ(wz3100)), :%(Pos(Zero), Neg(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe22(wz134, wz3100, wz41110100, wz3100, wz41111)
new_listToMaybe24(wz134, Neg(Zero), Neg(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
new_listToMaybe19(Neg(Succ(wz3100)), :%(Pos(Zero), Neg(Zero)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
new_listToMaybe23(wz134, wz31, wz411101, wz41111) → new_listToMaybe20(wz134, wz31, wz41111, wz134)
new_listToMaybe20(wz116, wz31, :(wz41110, wz41111), wz117) → new_listToMaybe19(wz31, wz41110, wz41111, new_primPlusNat(wz117), new_primPlusNat(wz117))
new_listToMaybe19(wz31, :%(Pos(Succ(wz41110000)), wz411101), wz41111, wz135, wz134) → new_listToMaybe20(wz134, wz31, wz41111, wz134)
new_listToMaybe24(wz134, Neg(Succ(wz3100)), Neg(Zero), wz41111) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
new_listToMaybe19(Pos(Succ(wz3100)), :%(Pos(Zero), Pos(Zero)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
new_listToMaybe19(Pos(Succ(wz3100)), :%(Pos(Zero), Pos(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe21(wz134, wz3100, wz41110100, wz3100, wz41111)
new_listToMaybe19(Pos(Succ(wz3100)), :%(Pos(Zero), Neg(wz4111010)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
new_listToMaybe24(wz134, Neg(Succ(wz3100)), Pos(wz4111010), wz41111) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
new_listToMaybe19(Pos(Zero), :%(Pos(Zero), Pos(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
new_listToMaybe24(wz134, Pos(Succ(wz3100)), Neg(wz4111010), wz41111) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
new_listToMaybe19(Neg(Zero), :%(Pos(Zero), Neg(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
new_listToMaybe19(Neg(Zero), :%(Pos(Zero), Pos(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)
new_listToMaybe19(Pos(Zero), :%(Pos(Zero), Neg(Succ(wz41110100))), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
new_listToMaybe21(wz230, Zero, Succ(wz2320), wz233, wz234) → new_listToMaybe20(wz230, Pos(Succ(wz233)), wz234, wz230)
new_listToMaybe21(wz230, Succ(wz2310), Zero, wz233, wz234) → new_listToMaybe20(wz230, Pos(Succ(wz233)), wz234, wz230)
new_listToMaybe24(wz134, Pos(Succ(wz3100)), Pos(Zero), wz41111) → new_listToMaybe20(wz134, Pos(Succ(wz3100)), wz41111, wz134)
new_listToMaybe24(wz134, Pos(Zero), Pos(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
new_listToMaybe22(wz236, Zero, Succ(wz2380), wz239, wz240) → new_listToMaybe20(wz236, Neg(Succ(wz239)), wz240, wz236)
new_listToMaybe22(wz236, Succ(wz2370), Zero, wz239, wz240) → new_listToMaybe20(wz236, Neg(Succ(wz239)), wz240, wz236)
new_listToMaybe19(wz31, :%(Neg(Succ(wz41110000)), wz411101), wz41111, wz135, wz134) → new_listToMaybe23(wz134, wz31, wz411101, wz41111)
new_listToMaybe24(wz134, Pos(Zero), Neg(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Pos(Zero), wz41111, wz134)
new_listToMaybe19(Neg(Succ(wz3100)), :%(Pos(Zero), Pos(wz4111010)), wz41111, wz135, wz134) → new_listToMaybe20(wz134, Neg(Succ(wz3100)), wz41111, wz134)
new_listToMaybe21(wz230, Succ(wz2310), Succ(wz2320), wz233, wz234) → new_listToMaybe21(wz230, wz2310, wz2320, wz233, wz234)
new_listToMaybe22(wz236, Succ(wz2370), Succ(wz2380), wz239, wz240) → new_listToMaybe22(wz236, wz2370, wz2380, wz239, wz240)
new_listToMaybe24(wz134, Neg(Succ(wz3100)), Neg(Succ(wz41110100)), wz41111) → new_listToMaybe22(wz134, wz3100, wz41110100, wz3100, wz41111)
new_listToMaybe24(wz134, Pos(Succ(wz3100)), Pos(Succ(wz41110100)), wz41111) → new_listToMaybe21(wz134, wz3100, wz41110100, wz3100, wz41111)
new_listToMaybe24(wz134, Neg(Zero), Pos(Succ(wz41110100)), wz41111) → new_listToMaybe20(wz134, Neg(Zero), wz41111, wz134)

The TRS R consists of the following rules:

new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe25(wz202, Zero, Zero, Neg(Zero), Pos(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Zero), wz208)
new_listToMaybe26(wz130, wz31, wz411101, wz3000, :(wz411110, wz411111)) → new_listToMaybe30(wz3000, wz31, wz411110, wz411111, wz130, wz130)
new_listToMaybe25(wz202, Zero, Zero, Neg(Succ(wz20500)), Neg(Zero), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Succ(wz20500)), wz208)
new_listToMaybe31(wz3000, wz31, :%(Neg(wz4111000), wz411101), :(wz411110, wz411111), wz131, wz130) → new_listToMaybe30(wz3000, wz31, wz411110, wz411111, wz130, wz130)
new_listToMaybe25(wz202, Zero, Zero, Pos(Zero), Pos(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Zero), wz208)
new_listToMaybe27(wz280, Zero, Succ(wz2820), wz283, wz284, wz285) → new_listToMaybe28(wz280, wz283, Pos(Succ(wz284)), wz285)
new_listToMaybe27(wz280, Succ(wz2810), Zero, wz283, wz284, wz285) → new_listToMaybe28(wz280, wz283, Pos(Succ(wz284)), wz285)
new_listToMaybe27(wz280, Succ(wz2810), Succ(wz2820), wz283, wz284, wz285) → new_listToMaybe27(wz280, wz2810, wz2820, wz283, wz284, wz285)
new_listToMaybe28(wz130, wz3000, wz31, :(wz411110, wz411111)) → new_listToMaybe30(wz3000, wz31, wz411110, wz411111, wz130, wz130)
new_listToMaybe25(wz202, Zero, Zero, Neg(Zero), Neg(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Zero), wz208)
new_listToMaybe25(wz202, Zero, Zero, Pos(Succ(wz20500)), Pos(Succ(wz20600)), wz207, wz208) → new_listToMaybe27(wz202, wz20500, wz20600, wz207, wz20500, wz208)
new_listToMaybe25(wz202, Succ(wz2030), Succ(wz2040), wz205, wz206, wz207, wz208) → new_listToMaybe25(wz202, wz2030, wz2040, wz205, wz206, wz207, wz208)
new_listToMaybe29(wz287, Succ(wz2880), Zero, wz290, wz291, wz292) → new_listToMaybe28(wz287, wz290, Neg(Succ(wz291)), wz292)
new_listToMaybe29(wz287, Zero, Succ(wz2890), wz290, wz291, wz292) → new_listToMaybe28(wz287, wz290, Neg(Succ(wz291)), wz292)
new_listToMaybe25(wz202, Zero, Zero, Pos(Succ(wz20500)), Pos(Zero), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Succ(wz20500)), wz208)
new_listToMaybe25(wz202, Zero, Succ(wz2040), wz205, wz206, wz207, wz208) → new_listToMaybe26(wz202, wz205, wz206, wz207, wz208)
new_listToMaybe25(wz202, Succ(wz2030), Zero, wz205, wz206, wz207, wz208) → new_listToMaybe26(wz202, wz205, wz206, wz207, wz208)
new_listToMaybe25(wz202, Zero, Zero, Pos(Zero), Neg(Succ(wz20600)), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Zero), wz208)
new_listToMaybe31(wz3000, wz31, :%(Pos(Zero), wz411101), wz41111, wz131, wz130) → new_listToMaybe26(wz130, wz31, wz411101, wz3000, wz41111)
new_listToMaybe25(wz202, Zero, Zero, Pos(Succ(wz20500)), Neg(wz2060), wz207, wz208) → new_listToMaybe28(wz202, wz207, Pos(Succ(wz20500)), wz208)
new_listToMaybe30(wz3000, wz31, wz41110, wz41111, wz120, wz121) → new_listToMaybe31(wz3000, wz31, wz41110, wz41111, new_primPlusNat(wz120), new_primPlusNat(wz120))
new_listToMaybe31(wz3000, wz31, :%(Pos(Succ(wz41110000)), wz411101), wz41111, wz131, wz130) → new_listToMaybe25(wz130, wz3000, wz41110000, wz31, wz411101, wz3000, wz41111)
new_listToMaybe25(wz202, Zero, Zero, Neg(Succ(wz20500)), Neg(Succ(wz20600)), wz207, wz208) → new_listToMaybe29(wz202, wz20500, wz20600, wz207, wz20500, wz208)
new_listToMaybe25(wz202, Zero, Zero, Neg(Succ(wz20500)), Pos(wz2060), wz207, wz208) → new_listToMaybe28(wz202, wz207, Neg(Succ(wz20500)), wz208)
new_listToMaybe29(wz287, Succ(wz2880), Succ(wz2890), wz290, wz291, wz292) → new_listToMaybe29(wz287, wz2880, wz2890, wz290, wz291, wz292)

The TRS R consists of the following rules:

new_primPlusNat(Zero) → Succ(Zero)
new_primPlusNat0(Succ(wz6100)) → Succ(wz6100)
new_primPlusNat(Succ(wz610)) → Succ(Succ(new_primPlusNat0(wz610)))
new_primPlusNat0(Zero) → Zero

The set Q consists of the following terms:

new_primPlusNat(Zero)
new_primPlusNat0(Zero)
new_primPlusNat(Succ(x0))
new_primPlusNat0(Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: